Nuprl Lemma : atom-free-ma-state 0,22
A:MsgA. AtomFree(ds(A))  AtomFree(Type;A.state) 
latex

DefinitionsM.state, AtomFree(T;x), Type, product-deq(A;B;a;b), proddeq(a;b), prod-deq(A;B;a;b), Atom, , {x:A| B(x) }, , AB, A, x:AB(x), False, Void, a<b, #$n, AtomDeq, atom-deq-aux, NatDeq, <a,b>, nat-deq-aux, x.A(x), f(a), AtomFree(d), Id, IdDeq, ds(M), MsgA, x:A. B(x), P  Q, t  T, State(ds), s ~ t, M.ds(x), x:AB(x)
Lemmasatom-free-Id, ma-ds wf, atom-free-ma-ds, msga wf, ma ds wf, id-deq wf, Id wf, atom-free-decl wf

origin